package at.tasat.cnf;

import java.util.BitSet;
import java.util.Iterator;

import at.tasat.util.ArrayIterator;

public final class Cnf implements Iterable<Clause> {

	private final Clause[] clauses;
	private final int numVariables;

	public Cnf(Clause[] clauses) {
		this.clauses = clauses.clone();
		
		BitSet hasVariable = new BitSet();
		int maxVariableId = 0;
		for (Clause clause : this.clauses) {
			for (int i = 0; i < clause.getNumberOfLiterals(); i++) {
				int variableId = Literal.getVariableId(clause.getLiteral(i));
				if (variableId > maxVariableId) {
					maxVariableId = variableId;
				}
				hasVariable.set(variableId);
			}
		}
		numVariables = maxVariableId;
		
		for (int i = 1; i <= numVariables; i++) {
			if (!hasVariable.get(i)) {
				throw new IllegalArgumentException("Not all variables used");
			}
		}
	}

	public int getNumberOfVariables() {
		return numVariables;
	}

	public int getNumberOfClauses() {
		return clauses.length;
	}

	public Clause getClause(int index) {
		return clauses[index];
	}
	
	@Override
	public Iterator<Clause> iterator() {
		return new ArrayIterator<Clause>(clauses);
	}

	@Override
	public String toString() {
		StringBuilder clausesBuilder = new StringBuilder();
		for (Clause clause : clauses) {
			clausesBuilder.append(clause);
			clausesBuilder.append('\n');
		}
		return clausesBuilder.toString().trim();
	}
}
